\begin{tabbing}
$\forall$${\it MA}$:MsgA, $s$:${\it MA}$.state, $k$:Knd, $l$:IdLnk, ${\it vaal}$:${\it MA}$.V($k$), $i$:Id.
\\[0ex]source($l$) $=$ $i$
\\[0ex]$\Rightarrow$ \=${\it MA}$.send($k$;\+
\\[0ex]$l$;$s$;${\it vaal}$;map($\lambda$$x$.2of($x$);filter($\lambda$${\it ms}$.eqof(IdLnkDeq)(mlnk(${\it ms}$),$l$);${\it MA}$.sends($k$,$s$,${\it vaal}$)));$i$)
\-
\end{tabbing}